perm filename WISEMA.PRF[F75,JMC] blob
sn#199786 filedate 1976-01-30 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00002 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002
C00019 ENDMK
C⊗;
*****∀E KW S,P,W;
1 T(KW(S,P),W)≡(T(K(S,P),W)∨T(K(S,NOT(P)),W))
*****∀E REFLEX S,W;
2 A(S,W,W)
*****∀E KNOW S,NOT(P),W;
3 T(K(S,NOT(P)),W)≡∀W1.(A(S,W,W1)⊃T(NOT(P),W1))
*****∀E NOT W,P;
4 T(NOT(P),W)≡¬T(P,W)
*****ASSUME T(K(S,NOT(P)),W);
5 T(K(S,NOT(P)),W) (5)
***** 3,5;
6 ∀W1.(A(S,W,W1)⊃T(NOT(P),W1)) (5)
*****∀E ↑ W;
7 A(S,W,W)⊃T(NOT(P),W) (5)
*****⊃E 2,↑;
8 T(NOT(P),W) (5)
*****⊃I 5⊃↑;
9 T(K(S,NOT(P)),W)⊃T(NOT(P),W)
***** 1,4,9;
10 (T(P,W)∧T(KW(S,P),W))⊃T(K(S,P),W)
*****LABEL (KW1 . 11);
*****∀I ↑ S P W;
11 ∀S P W.((T(P,W)∧T(KW(S,P),W))⊃T(K(S,P),W))
*****∀E KNOW S,P,W;
12 T(K(S,P),W)≡∀W1.(A(S,W,W1)⊃T(P,W1))
*****ASSUME T(K(S,P),W);
13 T(K(S,P),W) (13)
***** 12:13;
14 ∀W1.(A(S,W,W1)⊃T(P,W1)) (13)
*****∀E ↑ W;
15 A(S,W,W)⊃T(P,W) (13)
*****⊃E 2,↑;
16 T(P,W) (13)
*****⊃I 13⊃↑;
17 T(K(S,P),W)⊃T(P,W)
*****LABEL (KNOWTRUE . 18);
*****∀I ↑ S P W;
18 ∀S P W.(T(K(S,P),W)⊃T(P,W))
*****∀E ↑ FOOL,KW(WISE3,WHITE1),RW;
19 T(K(FOOL,KW(WISE3,WHITE1)),RW)⊃T(KW(WISE3,WHITE1),RW)
*****∀E ↑↑ FOOL,KW(WISE3,WHITE2),RW;
20 T(K(FOOL,KW(WISE3,WHITE2)),RW)⊃T(KW(WISE3,WHITE2),RW)
*****∀E 11 WISE3,WHITE1,RW;
21 (T(WHITE1,RW)∧T(KW(WISE3,WHITE1),RW))⊃T(K(WISE3,WHITE1),RW)
*****∀E 11 WISE3,WHITE2,RW;
22 (T(WHITE2,RW)∧T(KW(WISE3,WHITE2),RW))⊃T(K(WISE3,WHITE2),RW)
***** WISEMAN6,WISEMAN1,19,21;
23 T(K(WISE3,WHITE1),RW)
***** WISEMAN7,WISEMAN1,20,22;
24 T(K(WISE3,WHITE2),RW)
*****LABEL (ASS1 . 25);
*****ASSUME A(WISE3,RW,W1);
25 A(WISE3,RW,W1) (25)
*****∀E KNOW WISE3,WHITE1,RW;
26 T(K(WISE3,WHITE1),RW)≡∀W1.(A(WISE3,RW,W1)⊃T(WHITE1,W1))
*****∀E KNOW WISE3,WHITE2,RW;
27 T(K(WISE3,WHITE2),RW)≡∀W1.(A(WISE3,RW,W1)⊃T(WHITE2,W1))
***** 23,26;
28 ∀W1.(A(WISE3,RW,W1)⊃T(WHITE1,W1))
***** 24,27;
29 ∀W1.(A(WISE3,RW,W1)⊃T(WHITE2,W1))
*****∀E ↑↑ W1;
30 A(WISE3,RW,W1)⊃T(WHITE1,W1)
*****∀E ↑↑ W1;
31 A(WISE3,RW,W1)⊃T(WHITE2,W1)
*****⊃E 25,↑↑;
32 T(WHITE1,W1) (25)
*****⊃E 25,↑↑;
33 T(WHITE2,W1) (25)
*****∀E KNOW WISE3,K(WISE2,NOT(K(WISE1,WHITE1))),RW;
34 T(K(WISE3,K(WISE2,NOT(K(WISE1,WHITE1)))),RW)≡∀W1.(A(WISE3,RW,W1)⊃T(K(WISE2,NOT(K(WISE1,WHITE1))),W1))
*****∀E KNOW WISE3,NOT(K(WISE2,WHITE2)),RW;
35 T(K(WISE3,NOT(K(WISE2,WHITE2))),RW)≡∀W1.(A(WISE3,RW,W1)⊃T(NOT(K(WISE2,WHITE2)),W1))
***** WISEMAN9,34;
36 ∀W1.(A(WISE3,RW,W1)⊃T(K(WISE2,NOT(K(WISE1,WHITE1))),W1))
***** WISEMAN10,35;
37 ∀W1.(A(WISE3,RW,W1)⊃T(NOT(K(WISE2,WHITE2)),W1))
*****∀E ↑↑ W1;
38 A(WISE3,RW,W1)⊃T(K(WISE2,NOT(K(WISE1,WHITE1))),W1)
*****∀E ↑↑ W1;
39 A(WISE3,RW,W1)⊃T(NOT(K(WISE2,WHITE2)),W1)
*****⊃E 25,↑↑;
40 T(K(WISE2,NOT(K(WISE1,WHITE1))),W1) (25)
*****⊃E 25,↑↑;
41 T(NOT(K(WISE2,WHITE2)),W1) (25)
*****∀E FOOL FOOL,P,W;
42 T(K(FOOL,P),W)⊃T(K(FOOL,K(FOOL,P)),W)
*****∀E FOOL S,K(FOOL,P),W;
43 T(K(FOOL,K(FOOL,P)),W)⊃T(K(FOOL,K(S,K(FOOL,P))),W)
*****∀E 18 FOOL,K(S,K(FOOL,P)),W;
44 T(K(FOOL,K(S,K(FOOL,P))),W)⊃T(K(S,K(FOOL,P)),W)
***** 42:44;
45 T(K(FOOL,P),W)⊃T(K(S,K(FOOL,P)),W)
*****LABEL (FOOL2 . 46);
*****∀I ↑ S W P;
46 ∀S W P.(T(K(FOOL,P),W)⊃T(K(S,K(FOOL,P)),W))
*****∀E KNOW S,K(FOOL,P),W;
47 T(K(S,K(FOOL,P)),W)≡∀W1.(A(S,W,W1)⊃T(K(FOOL,P),W1))
*****ASSUME T(K(FOOL,P),W);
48 T(K(FOOL,P),W) (48)
***** 45,47:48;
49 ∀W1.(A(S,W,W1)⊃T(K(FOOL,P),W1)) (48)
*****∀E ↑ W1;
50 A(S,W,W1)⊃T(K(FOOL,P),W1) (48)
*****⊃I ↑↑↑⊃↑;
51 T(K(FOOL,P),W)⊃(A(S,W,W1)⊃T(K(FOOL,P),W1))
***** 51;
52 (T(K(FOOL,P),W)∧A(S,W,W1))⊃T(K(FOOL,P),W1)
*****LABEL (FOOLTRANS . 53);
*****∀I ↑ S P W W1;
53 ∀S P W W1.((T(K(FOOL,P),W)∧A(S,W,W1))⊃T(K(FOOL,P),W1))
*****∀E ↑ WISE3,KW(WISE1,WHITE2),RW,W1;
54 (T(K(FOOL,KW(WISE1,WHITE2)),RW)∧A(WISE3,RW,W1))⊃T(K(FOOL,KW(WISE1,WHITE2)),W1)
*****∀E ↑↑ WISE3,KW(WISE1,WHITE3),RW,W1;
55 (T(K(FOOL,KW(WISE1,WHITE3)),RW)∧A(WISE3,RW,W1))⊃T(K(FOOL,KW(WISE1,WHITE3)),W1)
*****∀E ↑↑↑ WISE3,KW(WISE2,WHITE1),RW,W1;
56 (T(K(FOOL,KW(WISE2,WHITE1)),RW)∧A(WISE3,RW,W1))⊃T(K(FOOL,KW(WISE2,WHITE1)),W1)
*****∀E 53 WISE3,KW(WISE2,WHITE3),RW,W1;
57 (T(K(FOOL,KW(WISE2,WHITE3)),RW)∧A(WISE3,RW,W1))⊃T(K(FOOL,KW(WISE2,WHITE3)),W1)
*****∀E 53 WISE3,OR(WHITE1,OR(WHITE2,WHITE3)),RW,W1;
58 (T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),RW)∧A(WISE3,RW,W1))⊃T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W1)
***** WISEMAN2,25,54;
59 T(K(FOOL,KW(WISE1,WHITE2)),W1) (25)
***** WISEMAN3,25,55;
60 T(K(FOOL,KW(WISE1,WHITE3)),W1) (25)
***** WISEMAN4,25,56;
61 T(K(FOOL,KW(WISE2,WHITE1)),W1) (25)
***** WISEMAN5,25,57;
62 T(K(FOOL,KW(WISE2,WHITE3)),W1) (25)
***** WISEMAN8,25,58;
63 T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W1) (25)
*****∀E KNOW WISE2,WHITE2,W1;
64 T(K(WISE2,WHITE2),W1)≡∀W.(A(WISE2,W1,W)⊃T(WHITE2,W))
*****∀E NOT W1,K(WISE2,WHITE2);
65 T(NOT(K(WISE2,WHITE2)),W1)≡¬T(K(WISE2,WHITE2),W1)
***** 41,64:65;
66 ¬∀W.(A(WISE2,W1,W)⊃T(WHITE2,W)) (25)
*****UNIFY↑;
67 ∃W.¬(A(WISE2,W1,W)⊃T(WHITE2,W)) (25)
*****∃E ↑ (W2);
68 ¬(A(WISE2,W1,W2)⊃T(WHITE2,W2)) (68)
***** 68;
69 A(WISE2,W1,W2) (68)
***** 68;
70 ¬T(WHITE2,W2) (68)
*****∀E 18 FOOL,KW(WISE2,WHITE1),W1;
71 T(K(FOOL,KW(WISE2,WHITE1)),W1)⊃T(KW(WISE2,WHITE1),W1)
*****∀E 11 WISE2,WHITE1,W1;
72 (T(WHITE1,W1)∧T(KW(WISE2,WHITE1),W1))⊃T(K(WISE2,WHITE1),W1)
*****∀E KNOW WISE2,WHITE1,W1;
73 T(K(WISE2,WHITE1),W1)≡∀W.(A(WISE2,W1,W)⊃T(WHITE1,W))
***** 32,61,71:73;
74 ∀W.(A(WISE2,W1,W)⊃T(WHITE1,W)) (25)
*****∀E ↑ W2;
75 A(WISE2,W1,W2)⊃T(WHITE1,W2) (25)
*****⊃E 69,↑;
76 T(WHITE1,W2) (25 68)
*****∀E KNOW WISE2,NOT(K(WISE1,WHITE1)),W1;
77 T(K(WISE2,NOT(K(WISE1,WHITE1))),W1)≡∀W.(A(WISE2,W1,W)⊃T(NOT(K(WISE1,WHITE1)),W))
***** 40,77;
78 ∀W.(A(WISE2,W1,W)⊃T(NOT(K(WISE1,WHITE1)),W)) (25)
*****∀E ↑ W2;
79 A(WISE2,W1,W2)⊃T(NOT(K(WISE1,WHITE1)),W2) (25)
*****⊃E 69,↑;
80 T(NOT(K(WISE1,WHITE1)),W2) (25 68)
*****∀E 53 WISE2,KW(WISE1,WHITE2),W1,W2;
81 (T(K(FOOL,KW(WISE1,WHITE2)),W1)∧A(WISE2,W1,W2))⊃T(K(FOOL,KW(WISE1,WHITE2)),W2)
*****∀E 53 WISE2,KW(WISE1,WHITE3),W1,W2;
82 (T(K(FOOL,KW(WISE1,WHITE3)),W1)∧A(WISE2,W1,W2))⊃T(K(FOOL,KW(WISE1,WHITE3)),W2)
*****∀E 53 WISE2,OR(WHITE1,OR(WHITE2,WHITE3)),W1,W2;
83 (T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W1)∧A(WISE2,W1,W2))⊃T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W2)
*****∀E 18 FOOL,KW(WISE1,WHITE2),W2;
84 T(K(FOOL,KW(WISE1,WHITE2)),W2)⊃T(KW(WISE1,WHITE2),W2)
*****∀E 18 FOOL,KW(WISE1,WHITE3),W2;
85 T(K(FOOL,KW(WISE1,WHITE3)),W2)⊃T(KW(WISE1,WHITE3),W2)
***** 59,68,81,84;
86 T(KW(WISE1,WHITE2),W2) (25 68)
***** 60,68,82,85;
87 T(KW(WISE1,WHITE3),W2) (25 68)
***** 63,68,83;
88 T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W2) (25 68)
*****∀E KW WISE1,WHITE2,W2;
89 T(KW(WISE1,WHITE2),W2)≡(T(K(WISE1,WHITE2),W2)∨T(K(WISE1,NOT(WHITE2)),W2))
*****∀E 18 WISE1,WHITE2,W2;
90 T(K(WISE1,WHITE2),W2)⊃T(WHITE2,W2)
***** 70,86,89:90;
91 T(K(WISE1,NOT(WHITE2)),W2) (25 68)
*****∀E KNOW WISE1,WHITE1,W2;
92 T(K(WISE1,WHITE1),W2)≡∀W1.(A(WISE1,W2,W1)⊃T(WHITE1,W1))
*****∀E NOT W2,K(WISE1,WHITE1);
93 T(NOT(K(WISE1,WHITE1)),W2)≡¬T(K(WISE1,WHITE1),W2)
***** 80,92:93;
94 ¬∀W1.(A(WISE1,W2,W1)⊃T(WHITE1,W1)) (25 68)
*****UNIFY↑;
95 ∃W1.¬(A(WISE1,W2,W1)⊃T(WHITE1,W1)) (25 68)
*****∃E ↑ (W3);
96 ¬(A(WISE1,W2,W3)⊃T(WHITE1,W3)) (96)
***** 96;
97 A(WISE1,W2,W3) (96)
***** 96;
98 ¬T(WHITE1,W3) (96)
*****∀E KNOW WISE1,NOT(WHITE2),W2;
99 T(K(WISE1,NOT(WHITE2)),W2)≡∀W1.(A(WISE1,W2,W1)⊃T(NOT(WHITE2),W1))
***** 91,99;
100 ∀W1.(A(WISE1,W2,W1)⊃T(NOT(WHITE2),W1)) (25 68)
*****∀E ↑ W3;
101 A(WISE1,W2,W3)⊃T(NOT(WHITE2),W3) (25 68)
*****∀E NOT W3,WHITE2;
102 T(NOT(WHITE2),W3)≡¬T(WHITE2,W3)
***** 97,101:102;
103 ¬T(WHITE2,W3) (25 68 96)
*****∀E 53 WISE1,OR(WHITE1,OR(WHITE2,WHITE3)),W2,W3;
104 (T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W2)∧A(WISE1,W2,W3))⊃T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W3)
***** 88,97,104;
105 T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W3) (25 68 96)
*****∀E 18 FOOL,OR(WHITE1,OR(WHITE2,WHITE3)),W3;
106 T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W3)⊃T(OR(WHITE1,OR(WHITE2,WHITE3)),W3)
*****∀E OR W3,WHITE1,OR(WHITE2,WHITE3);
107 T(OR(WHITE1,OR(WHITE2,WHITE3)),W3)≡(T(WHITE1,W3)∨T(OR(WHITE2,WHITE3),W3))
*****∀E OR W3,WHITE2,WHITE3;
108 T(OR(WHITE2,WHITE3),W3)≡(T(WHITE2,W3)∨T(WHITE3,W3))
***** 98,103,105:108;
109 T(WHITE3,W3) (25 68 96)
*****∀E KW WISE1,WHITE3,W2;
110 T(KW(WISE1,WHITE3),W2)≡(T(K(WISE1,WHITE3),W2)∨T(K(WISE1,NOT(WHITE3)),W2))
*****∀E KNOW WISE1,NOT(WHITE3),W2;
111 T(K(WISE1,NOT(WHITE3)),W2)≡∀W1.(A(WISE1,W2,W1)⊃T(NOT(WHITE3),W1))
*****ASSUME ∀W1.(A(WISE1,W2,W1)⊃T(NOT(WHITE3),W1));
112 ∀W1.(A(WISE1,W2,W1)⊃T(NOT(WHITE3),W1)) (112)
*****∀E ↑ W3;
113 A(WISE1,W2,W3)⊃T(NOT(WHITE3),W3) (112)
*****∀E NOT W3,WHITE3;
114 T(NOT(WHITE3),W3)≡¬T(WHITE3,W3)
***** 97,109,113:114;
115 FALSE (25 68 112)
*****⊃I 112⊃↑;
116 ∀W1.(A(WISE1,W2,W1)⊃T(NOT(WHITE3),W1))⊃FALSE (25 68)
***** 87,110:111,116;
117 T(K(WISE1,WHITE3),W2) (25 68)
*****∀E 18 WISE1,WHITE3,W2;
118 T(K(WISE1,WHITE3),W2)⊃T(WHITE3,W2)
*****⊃E ↑↑,↑;
119 T(WHITE3,W2) (25 68)
*****∀E 18 FOOL,KW(WISE2,WHITE3),W1;
120 T(K(FOOL,KW(WISE2,WHITE3)),W1)⊃T(KW(WISE2,WHITE3),W1)
*****∀E KW WISE2,WHITE3,W1;
121 T(KW(WISE2,WHITE3),W1)≡(T(K(WISE2,WHITE3),W1)∨T(K(WISE2,NOT(WHITE3)),W1))
*****∀E KNOW WISE2,NOT(WHITE3),W1;
122 T(K(WISE2,NOT(WHITE3)),W1)≡∀W.(A(WISE2,W1,W)⊃T(NOT(WHITE3),W))
*****ASSUME ∀W.(A(WISE2,W1,W)⊃T(NOT(WHITE3),W));
123 ∀W.(A(WISE2,W1,W)⊃T(NOT(WHITE3),W)) (123)
*****∀E ↑ W2;
124 A(WISE2,W1,W2)⊃T(NOT(WHITE3),W2) (123)
*****∀E NOT W2,WHITE3;
125 T(NOT(WHITE3),W2)≡¬T(WHITE3,W2)
***** 69,119,124:125;
126 FALSE (25 123)
*****⊃I 123⊃↑;
127 ∀W.(A(WISE2,W1,W)⊃T(NOT(WHITE3),W))⊃FALSE (25)
***** 62,120:122,127;
128 T(K(WISE2,WHITE3),W1) (25)
*****∀E 18 WISE2,WHITE3,W1;
129 T(K(WISE2,WHITE3),W1)⊃T(WHITE3,W1)
*****⊃E ↑↑,↑;
130 T(WHITE3,W1) (25)
*****⊃I 25⊃↑;
131 A(WISE3,RW,W1)⊃T(WHITE3,W1)
*****∀I ↑ W1;
132 ∀W1.(A(WISE3,RW,W1)⊃T(WHITE3,W1))
*****∀E KNOW WISE3,WHITE3,RW;
133 T(K(WISE3,WHITE3),RW)≡∀W1.(A(WISE3,RW,W1)⊃T(WHITE3,W1))
***** 132:133;
134 T(K(WISE3,WHITE3),RW)